  \documentclass{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{myproof}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}
\usepackage{davidemacro}
\usepackage{evolvablemacro}


\usepackage{color}
\newcommand{\emphcolor}[1]{\textcolor{magenta}{#1}\xspace}

\title[Adaptable Processes]{Adaptable Processes}
\author[Cinzia Di Giusto]{ M. Bravetti \and \emphcolor{Cinzia Di Giusto} \and J. A. P\'erez \and G. Zavattaro}
\date[]{FMOODS-FORTE 2011 -- Reykjavik}
  
\institute[INRIA Rh\^onealpes]{Universit\`a di Bologna,
INRIA Rh\^{o}ne-Alpes, 
FCT New University of Lisbon}

\setbeamertemplate{navigation symbols}{} 

\usecolortheme{crane}
\useoutertheme{progressbar}
\useinnertheme{progressbar}
\usefonttheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}

\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}
\newcommand{\whitecolor}[1]{\textcolor{white}{#1}\xspace}
\newcommand{\hidecolor}[1]{\textcolor{darkgray}{#1}\xspace}
\newcommand{\olivecolor}[1]{\textcolor{orange}{#1}\xspace}

%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,

\newcommand{\tealtext}[1]{\textcolor{teal}{#1}\xspace}

\newcommand{\str}[1]{\structure{#1}}


%\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}
%\newcommand{\til}[1]{\widetilde{#1}}
%\newcommand{\update}[2]{\til{#1}\{#2\} } 
%\newcommand{\component}[2]{#1 [#2]   }  %a[P]
%\newcommand{\outC}[1]{\overline{#1}}      % CCS  output

\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\bbl}[1]{\begin{block}{#1}}
\newcommand{\ebl}{\end{block}}

% Context
\newcommand{\ol}{\langle\!\langle}
\newcommand{\cl}{\rangle\!\rangle}
\newcommand{\hl}[1]{\ol #1 \cl}
\newcommand{\fillcon}[2]{\ensuremath{#1\hl{#2}}}

\newcommand{\pired}{\longrightarrow}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\rulename}[1]{\textsc{(#1)}}

\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\midef}{\ensuremath{\stackrel{\mathsf{def}}{=}}}



%\newcommand{\str}[1]{\structure{#1}}
\newcommand{\fkspc}{{\tiny \ }\\}





\begin{document}

\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}

\begin{frame}
\frametitle{Roadmap}

\tableofcontents

\end{frame}

\section{Motivation}

\begin{frame}
\frametitle{Context (very broad)}

Modern computing systems are increasingly
\begin{itemize}
\item concurrent
\begin{itemize}
\item multiple interacting entities, usually distributed 
\end{itemize}
\vspace{0.2cm}
\item infinite 
\begin{itemize}
\item termination is a \emphcolor{local} property
\item tolerant to \emphcolor{unexpected conditions} (e.g. failures)
\item but also able to \emphcolor{dynamically reconfigure} themselves \\ (e.g. performance and maintenance reasons)
\end{itemize}
\end{itemize}
\end{frame}


\frame{
\frametitle{Our approach}
%A \str{} to the analysis of \str{evolvable systems} 


We are mainly concerned with \emphcolor{dynamic reconfiguration} issues:\\
\vspace{0.2cm}
\begin{itemize}
\item finding proper \emphcolor{evolution/reconfiguration} mechanisms 
\vspace{0.2cm}
\item understanding the \emphcolor{properties} evolvable systems should ensure 
\end{itemize}
 \pause
\begin{block}{Our proposal}
\begin{itemize}
\item A \emphcolor{process calculus} of adaptable processes, called \emphcolorb{\evol{}} 
\vspace{0.2cm}
\item \emphcolor{Verification problems} for evolvable systems defined in \evol{} 
\vspace{0.2cm}
\item \emphcolor{(Un)decidability results} for such problems
\end{itemize}
\end{block}

}

\frame{
\frametitle{Dynamic reconfiguration is important}
It is \emphcolor{everywhere}:
\vspace{0.2cm}
\bi
\item Process scheduling in OS
\vspace{0.2cm}
\item Hot update in component-based systems
\vspace{0.2cm}
\item Workflow applications
\vspace{0.2cm}
\item Cloud computing
\vspace{0.2cm}
\item \dots
\ei

%\pause 

%\emphcolorb{Claim:} Existing process calculi do not properly capture dynamic reconfiguration.
}

\begin{frame}
\frametitle{What is dynamic in known process calculi?}

\begin{center}
Essentially, the \emphcolor{communication topology}. 
\end{center}

Some examples:
\vspace{0.2cm}
\begin{itemize}
  \item CCS: interacting concurrent processes in a \emphcolor{static topology}
\vspace{0.5cm}  
  \item The $\pi$-calculus: \emphcolor{dynamic network topologies} through channel/link mobility
%  \vspace{0.5cm}
  \vspace{0.5cm}
  \item The Ambient calculus: \emphcolor{dynamic spatial topologies} through ambient  mobility
  %(dynamic behaviors depending on the position)
%\vspace{0.5cm}
\end{itemize}


%What about \emphcolor{dynamic reconfiguration}?
%Dynamic reconfiguration does not really fit in any of these abstractions
%  \item but what about dynamic behaviors? How to describe a process that changes along time?

\end{frame}


\section{Adaptable Processes}


\begin{frame}
\frametitle{Adaptable processes}

\begin{block}{}
An \emphcolor{adaptable process} describes all the scenarios where:

\begin{itemize}
  \item a direct manipulation of the process is required,
  
  \item processes could be stopped, restarted, modified along time.
\end{itemize}
\end{block}

% \vspace{0.5cm}
% 
% For instance, they can be used to model:
% \begin{itemize}
% 
% \item Workflow applications,
% 
% \item Cloud applications,
% 
% \item Hot updates in component-based systems,
% 
% \item \dots
% \end{itemize}


\end{frame}





\begin{frame}[t]
\frametitle{A calculus for adaptable processes }

\begin{block}{Syntax}
CCS without restriction \only<2->{plus \emphcolor{localities}}\only<3->{ and \emphcolorb{update prefixes}:}
$$
\begin{array}{ll}
P        ::=& \sum_{i \in I} \pi_i.P_i   \, \mid \, 
          P \parallel P  \, \mid \, ! \pi.P \, \only<2->{\mid \, \emphcolor{\component{a}{P}}}\\ \\
\pi   ::=&  a \, \mid \, \outC{a} \only<3->{\, \mid \, \emphcolorb{\update{a}{U}}}
\end{array}
$$
\only<3->{where 
\begin{itemize}
\item $\component{a}{P}$ is the \emphcolor{adaptable process} $P$ \emphcolor{located at} name $a$
\item $U$ is a \emphcolorb{context}, with zero or more \emphcolorb{holes}, denoted $\bullet$
\end{itemize}}
\end{block}

\end{frame}








\begin{frame}
\frametitle{Operational Semantics: Intuitions}

\begin{block}{Locations}
\begin{itemize}
\item The localities are \emphcolor{transparent}:
$$
 \rightinfer
 			{\component{a}{P} \xrightarrow{~\alpha~}  \component{a}{P'}}
 			{P \xrightarrow{~\alpha~} P'} 
			$$
\end{itemize}			
\end{block}

\pause

\begin{block}{Reconfiguration}
\begin{itemize}

\item Dynamic reconfiguration is obtained  via an interaction  with update prefixes:
$$
\component{a}{P} \parallel \update{a}{U}.Q \xrightarrow{~\tau~} \fillcon{U}{P} \parallel Q
$$

\item{Process $\fillcon{U}{P}$ is obtained by filling in the holes in $U$ with $P$}
%\item An update replaces an adaptable process with a
%new process filled with the process currently
%active in the updated location
%
%\end{itemize}
%
%metti sintassi di techrep
% $$
%\begin{array}{c}
% \component{a}{P} \xrightarrow{~\component{a}{P}~}  \star
%\qquad 
%\rightinfer
%			{P_1 \parallel P_2 \xrightarrow{~\tau~} P_1'\sub{ U \sub{Q}{\bullet}  }{\star} \parallel P_2'}
%			{P_1 \xrightarrow{~\component{a}{Q}~} P_1' \qquad P_2 \xrightarrow{~\update{a}{U}~} P_2'}
%\end{array}
%$$
\end{itemize}
\end{block}

\end{frame}

\frame{
\frametitle{A calculus for adaptable processes}

\begin{block}{Operational Semantics: LTS}

%A Labeled Transition System (LTS) which extends that of C
$$
\fbox{\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}}
\qquad 
\fbox{\inferrule[\rulename{Tau3}]{P_1 \arro{~\component{a}{\emphcolor{Q}}~} P_1'\andalso P_2 \arro{~\update{a}{\emphcolorb{U}}~} P_2' }{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{\emphcolorb{U}}{\emphcolor{Q}}  }{\star} \parallel P_2'}}
$$
$$
\fbox{\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}}
\quad 
\hidecolor{\inferrule[\rulename{Act1}]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	}
\quad
\hidecolor{\inferrule[\rulename{Tau1}]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outC{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}}
$$
$$
\hidecolor{\inferrule[\rulename{Sum}]{}{\sum_{i\in I} \alpha_i.P_i \arro{~\alpha_i~}  P_i } }
\qquad
\hidecolor{\inferrule[\textsc{(Repl)}]{}{!\alpha.P \arro{~\alpha~}  P \parallel !\alpha.P }}
$$
\end{block}
}

\frame{
\frametitle{A first example}

A basic client-server scenario:   
\begin{align*}
& \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.C} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
\pired ~ & \componentbbig{client}{\component{run}{P} \parallel  C} \parallel \componentbbig{server}{\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
\pired ~ & \componentbbig{client}{\component{run}{Q \parallel old.P} \parallel C} \parallel \componentbbig{server}{S}
\end{align*}

}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1->[Deep update] $$\hspace{-55pt}\componentbbig{a}{Q \parallel \component{b}{R \parallel \emphcolor{\component{c}{S_{1}}}\, }\, } \parallel \update{c}{\component{d}{S'}}.\nil \pired \componentbbig{a}{Q \parallel \componentbbig{b}{R \parallel \emphcolor{\component{d}{S_{2}}}\, }\, } \parallel \nil $$
\item<2->[Destroyer]$$\quad \component{a}{P} \parallel \update{a}{Q}.R \pired Q \parallel R \quad (\bullet \not \in Q)$$
\item<3>[Plug-in] $$\component{a}{Q} \parallel \update{a}{\component{a}{c{.}\bullet +R}}.\nil \pired \component{a}{c{.}Q +\fillcon{R}{Q}} \parallel \nil$$ 
\end{description}
}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1->[Renaming] $$\component{m}{\component{a}{Q}} \parallel \component{n}{\update{a}{\component{b}{\bullet}}.S} \pired \component{m}{\component{b}{Q} }\parallel \component{m}{S}$$
\item<2->[Backup] $$\component{a}{Q} \parallel \update{a}{\component{a}{\bullet} \parallel \component{b}{\bullet}}.S \pired \component{a}{Q} \parallel \component{b}{Q} \parallel S$$
\item<3>[Replacement] $$\quad \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(\bullet \not \in R)$$ 


\end{description}
}



\begin{frame}
 \frametitle{A compelling example\\ Scaling in cloud computing}


\begin{itemize}
 \item An application in the cloud
$$
G  =  \componentbbig{g}{\, I \parallel \cdots \parallel I \parallel \emphcolor{S_{dw}} \parallel \emphcolor{S_{up}} \parallel \nmu{CTRL}_{i} \,}
$$

\vspace{0.5cm}

\item A way of controlling scaling
 $$
\begin{array}{l}
S_{dw}  =  \componentbbig{s_{d}}{\, !\,\nm{alert^{d}}.\prod^{j} \update{\nmu{mid}}{\nil}\, } \\
S_{up}  =  \componentbbig{s_{u}}{\, !\,\nm{alert^{u}}.\prod^{k} \updatebig{\nmu{mid}}{\component{\nmu{mid}}{\bullet} \parallel \component{\nmu{mid}}{\bullet}}\, }
 \end{array}
$$


\end{itemize}


 

\end{frame}



\section{Verification Problems}


\begin{frame}
\frametitle{Verification problems for adaptable processes}

An evolvable system is composed of:
\vspace{0.2cm}
\begin{itemize}
 \item an \emphcolor{initial configuration} $P$ 
\vspace{0.2cm}
 \item an arbitrary number of \emphcolorb{reconfigurations} $\mathcal{M}$
\end{itemize}
 \vspace{0.5cm}

\pause
\begin{itemize}
 \item We observe the system's behavior using \emphcolor{barbs}. 
\vspace{0.2cm}
 \item These observables represent \emphcolor{special signals}: errors, interrupts.

\end{itemize}



\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario}
\only<1>{\includegraphics[height=50mm]{cluster0.pdf}}
\only<2>{\includegraphics[height=50mm]{cluster2.pdf}}
\only<3>{\includegraphics[height=50mm]{cluster1.pdf}}
\only<4>{\includegraphics[height=50mm]{cluster3.pdf}}
\only<5>{\includegraphics[height=50mm]{cluster4.pdf}}
\end{frame}








\begin{frame}
\frametitle{Verification problems for adaptable processes}
Given:
\begin{itemize}
 \item an initial configuration $P$, 
 \item a set of reconfigurations,
 \item a special error signal $e$.
\end{itemize}

\vspace{0.2cm}
\begin{block}{}
\centering 
We would like to know if  for every reachable configuration exposing $e$ the system:

\begin{enumerate}
 \item  recovers in at most $k$ steps  (\emphcolor{bounded adaptation}),
\vspace{0.2cm}
 \item  eventually recovers  (\emphcolor{eventual adaptation}). 
\end{enumerate}
\end{block}
\end{frame}


\begin{frame}
 \frametitle{Decidability of the verification problems}

\begin{itemize}
 \item Bounded and eventual adaptation are \emphcolor{undecidable} in \evol{}
\vspace{0.5cm}

 \item The verification problems can be related to \emphcolor{termination} in Turing Complete models
\vspace{0.5cm}
 \item If a Turing machine $M$ terminates then its encoding into \evol{}, has
a computation where the error message is always available
 
\end{itemize}
\end{frame}


\begin{frame}
 \frametitle{Towards decidability}

\begin{itemize}
 \item Are there any fragments where something can be decided?
\vspace{0.5cm}
 \item \emphcolor{Intuition}: to disallow some update patterns\\
i.e. holes cannot appear behind prefixes
\vspace{0.5cm}
 \item The obtained fragment \evol{-} is still powerful enough to model interesting scenarios 

\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Some examples}
\begin{description}
\item[Replacement] $$\quad \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(\bullet \not \in R)$$ 
\item[Destroyer]$$\quad \component{a}{P} \parallel \update{a}{Q}.R \pired Q \parallel R \quad (\bullet \not \in Q)$$
\item[Renaming] $$\component{m}{\component{a}{Q}} \parallel \component{n}{\update{a}{\component{b}{\bullet}}.S} \pired \component{m}{\component{b}{Q} }\parallel \component{m}{S}$$
\item[Backup] $$\component{a}{Q} \parallel \update{a}{\component{a}{\bullet} \parallel \component{b}{\bullet}}.S \pired \component{a}{Q} \parallel \component{b}{Q} \parallel S$$
\end{description}

\end{frame}




\begin{frame}
\frametitle{Bounded adaptation is decidable in \evol{-}}

 \begin{center}
  The algorithm consists in checking whether it is  possible to \emphcolor{reach a
process greater} than one that exhibit at least $k$ signals
 \end{center}

This accounts in:
\begin{enumerate}
 \item  defining an ordering on states 
\vspace{0.2cm}
\item performing a symbolic backward analysis



\end{enumerate}
\begin{center}
\includegraphics[width=0.7\textwidth]{predanalisi.pdf} 
\end{center}
 

\end{frame}


\begin{frame}
 \frametitle{Eventual Adaptation is undecidable}

\begin{itemize}
 \item \evol{-} is weakly Turing powerful
\vspace{0.5cm}

\item Termination can be related to the eventual adaptation problem

\end{itemize}



\end{frame}



\section{Final remarks}
\begin{frame}
\frametitle{Concluding remarks}

\begin{itemize}
\item A process calculus approach to dynamic reconfiguration, evolvability, and adaptation
\vspace{0.2cm}
\item 
A basis for the development of more expressive languages, and for verification studies
\end{itemize}

\pause
\begin{block}{Further results}
\begin{itemize}
 \item  Decidability results for static and dynamic topologies of adaptable processes.
\begin{center}
Take a look at our TR at \emphcolor{\url{www.cs.unibo.it/~perez/ap/}} 
\end{center}

 \item Dynamic reconfiguration in \evol{} with  priorities/fairness, Type systems: safe updates

\end{itemize}

\end{block}
\end{frame}



\end{document}
